A:Type, eq:EqDecider(A), B:(AType), L:(a:A fp B(a) List), x:A.
(x  fpf-domain((L)))  (fL.(x  fpf-domain(f))) 

latex

Definitions	t  T, x:AB(x), x:A. B(x), (x  l), f(a), x(s), a:A fp B(a), (xL.P(x)), P  Q, x. t(x), type List, Type, EqDecider(T), x:A  B(x), P & Q, b, x:A. B(x), P  Q, P  Q, x.A(x), Top
Lemmas	fpf-trivial-subtype-top, iff functionality wrt iff, member-fpf-domain, fpf-join-list-dom, deq wf, fpf wf